0 CpxTRS
↳1 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxWeightedTrs
↳3 InnermostUnusableRulesProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxWeightedTrs
↳5 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳6 CpxTypedWeightedTrs
↳7 CompletionProof (UPPER BOUND(ID), 0 ms)
↳8 CpxTypedWeightedCompleteTrs
↳9 NarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
↳10 CpxTypedWeightedCompleteTrs
↳11 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)
↳12 CpxRNTS
↳13 InliningProof (UPPER BOUND(ID), 187 ms)
↳14 CpxRNTS
↳15 SimplificationProof (BOTH BOUNDS(ID, ID), 0 ms)
↳16 CpxRNTS
↳17 CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID), 0 ms)
↳18 CpxRNTS
↳19 IntTrsBoundProof (UPPER BOUND(ID), 261 ms)
↳20 CpxRNTS
↳21 IntTrsBoundProof (UPPER BOUND(ID), 36 ms)
↳22 CpxRNTS
↳23 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳24 CpxRNTS
↳25 IntTrsBoundProof (UPPER BOUND(ID), 34 ms)
↳26 CpxRNTS
↳27 IntTrsBoundProof (UPPER BOUND(ID), 26 ms)
↳28 CpxRNTS
↳29 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳30 CpxRNTS
↳31 IntTrsBoundProof (UPPER BOUND(ID), 203 ms)
↳32 CpxRNTS
↳33 IntTrsBoundProof (UPPER BOUND(ID), 16 ms)
↳34 CpxRNTS
↳35 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳36 CpxRNTS
↳37 IntTrsBoundProof (UPPER BOUND(ID), 45 ms)
↳38 CpxRNTS
↳39 IntTrsBoundProof (UPPER BOUND(ID), 77 ms)
↳40 CpxRNTS
↳41 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳42 CpxRNTS
↳43 IntTrsBoundProof (UPPER BOUND(ID), 359 ms)
↳44 CpxRNTS
↳45 IntTrsBoundProof (UPPER BOUND(ID), 97 ms)
↳46 CpxRNTS
↳47 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳48 CpxRNTS
↳49 IntTrsBoundProof (UPPER BOUND(ID), 283 ms)
↳50 CpxRNTS
↳51 IntTrsBoundProof (UPPER BOUND(ID), 37 ms)
↳52 CpxRNTS
↳53 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳54 CpxRNTS
↳55 IntTrsBoundProof (UPPER BOUND(ID), 88 ms)
↳56 CpxRNTS
↳57 IntTrsBoundProof (UPPER BOUND(ID), 6 ms)
↳58 CpxRNTS
↳59 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳60 CpxRNTS
↳61 IntTrsBoundProof (UPPER BOUND(ID), 579 ms)
↳62 CpxRNTS
↳63 IntTrsBoundProof (UPPER BOUND(ID), 189 ms)
↳64 CpxRNTS
↳65 ResultPropagationProof (UPPER BOUND(ID), 0 ms)
↳66 CpxRNTS
↳67 IntTrsBoundProof (UPPER BOUND(ID), 722 ms)
↳68 CpxRNTS
↳69 IntTrsBoundProof (UPPER BOUND(ID), 3 ms)
↳70 CpxRNTS
↳71 FinalProof (⇔, 0 ms)
↳72 BOUNDS(1, n^2)
from(X) → cons(X, n__from(s(X)))
2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, n__cons(Y, Z))) → rcons(posrecip(activate(Y)), 2ndsneg(N, activate(Z)))
2ndsneg(0, Z) → rnil
2ndsneg(s(N), cons(X, n__cons(Y, Z))) → rcons(negrecip(activate(Y)), 2ndspos(N, activate(Z)))
pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0
times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)
from(X) → n__from(X)
cons(X1, X2) → n__cons(X1, X2)
activate(n__from(X)) → from(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(X) → X
from(X) → cons(X, n__from(s(X))) [1]
2ndspos(0, Z) → rnil [1]
2ndspos(s(N), cons(X, n__cons(Y, Z))) → rcons(posrecip(activate(Y)), 2ndsneg(N, activate(Z))) [1]
2ndsneg(0, Z) → rnil [1]
2ndsneg(s(N), cons(X, n__cons(Y, Z))) → rcons(negrecip(activate(Y)), 2ndspos(N, activate(Z))) [1]
pi(X) → 2ndspos(X, from(0)) [1]
plus(0, Y) → Y [1]
plus(s(X), Y) → s(plus(X, Y)) [1]
times(0, Y) → 0 [1]
times(s(X), Y) → plus(Y, times(X, Y)) [1]
square(X) → times(X, X) [1]
from(X) → n__from(X) [1]
cons(X1, X2) → n__cons(X1, X2) [1]
activate(n__from(X)) → from(X) [1]
activate(n__cons(X1, X2)) → cons(X1, X2) [1]
activate(X) → X [1]
2ndspos(s(N), cons(X, n__cons(Y, Z))) → rcons(posrecip(activate(Y)), 2ndsneg(N, activate(Z))) [1]
2ndsneg(s(N), cons(X, n__cons(Y, Z))) → rcons(negrecip(activate(Y)), 2ndspos(N, activate(Z))) [1]
cons(X1, X2) → n__cons(X1, X2) [1]
from(X) → cons(X, n__from(s(X))) [1]
2ndspos(0, Z) → rnil [1]
2ndsneg(0, Z) → rnil [1]
pi(X) → 2ndspos(X, from(0)) [1]
plus(0, Y) → Y [1]
plus(s(X), Y) → s(plus(X, Y)) [1]
times(0, Y) → 0 [1]
times(s(X), Y) → plus(Y, times(X, Y)) [1]
square(X) → times(X, X) [1]
from(X) → n__from(X) [1]
cons(X1, X2) → n__cons(X1, X2) [1]
activate(n__from(X)) → from(X) [1]
activate(n__cons(X1, X2)) → cons(X1, X2) [1]
activate(X) → X [1]
from(X) → cons(X, n__from(s(X))) [1]
2ndspos(0, Z) → rnil [1]
2ndsneg(0, Z) → rnil [1]
pi(X) → 2ndspos(X, from(0)) [1]
plus(0, Y) → Y [1]
plus(s(X), Y) → s(plus(X, Y)) [1]
times(0, Y) → 0 [1]
times(s(X), Y) → plus(Y, times(X, Y)) [1]
square(X) → times(X, X) [1]
from(X) → n__from(X) [1]
cons(X1, X2) → n__cons(X1, X2) [1]
activate(n__from(X)) → from(X) [1]
activate(n__cons(X1, X2)) → cons(X1, X2) [1]
activate(X) → X [1]
from :: s:0 → n__from:n__cons cons :: s:0 → n__from:n__cons → n__from:n__cons n__from :: s:0 → n__from:n__cons s :: s:0 → s:0 2ndspos :: s:0 → n__from:n__cons → rnil 0 :: s:0 rnil :: rnil 2ndsneg :: s:0 → a → rnil pi :: s:0 → rnil plus :: s:0 → s:0 → s:0 times :: s:0 → s:0 → s:0 square :: s:0 → s:0 n__cons :: s:0 → n__from:n__cons → n__from:n__cons activate :: n__from:n__cons → n__from:n__cons |
(a) The obligation is a constructor system where every type has a constant constructor,
(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:
2ndspos
2ndsneg
pi
square
activate
times
from
plus
cons
const, const1
Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
0 => 0
rnil => 0
const => 0
const1 => 0
2ndsneg(z, z') -{ 1 }→ 0 :|: Z >= 0, z' = Z, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: Z >= 0, z' = Z, z = 0
activate(z) -{ 1 }→ X :|: X >= 0, z = X
activate(z) -{ 1 }→ from(X) :|: z = 1 + X, X >= 0
activate(z) -{ 1 }→ cons(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
cons(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
from(z) -{ 1 }→ cons(X, 1 + (1 + X)) :|: X >= 0, z = X
from(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
pi(z) -{ 2 }→ 2ndspos(X, cons(0, 1 + (1 + 0))) :|: X >= 0, z = X
pi(z) -{ 2 }→ 2ndspos(X, 1 + 0) :|: X >= 0, z = X
plus(z, z') -{ 1 }→ Y :|: z' = Y, Y >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(X, Y) :|: z = 1 + X, z' = Y, Y >= 0, X >= 0
square(z) -{ 1 }→ times(X, X) :|: X >= 0, z = X
times(z, z') -{ 2 }→ plus(Y, plus(Y, times(X', Y))) :|: z' = Y, Y >= 0, X' >= 0, z = 1 + (1 + X')
times(z, z') -{ 2 }→ plus(Y, 0) :|: z' = Y, Y >= 0, z = 1 + 0
times(z, z') -{ 1 }→ 0 :|: z' = Y, Y >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: Z >= 0, z' = Z, z = 0
cons(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
from(z) -{ 1 }→ cons(X, 1 + (1 + X)) :|: X >= 0, z = X
from(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
2ndsneg(z, z') -{ 1 }→ 0 :|: Z >= 0, z' = Z, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: Z >= 0, z' = Z, z = 0
activate(z) -{ 1 }→ X :|: X >= 0, z = X
activate(z) -{ 2 }→ cons(X', 1 + (1 + X')) :|: z = 1 + X, X >= 0, X' >= 0, X = X'
activate(z) -{ 2 }→ 1 + X' :|: z = 1 + X, X >= 0, X' >= 0, X = X'
activate(z) -{ 2 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
from(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
from(z) -{ 2 }→ 1 + X1 + X2 :|: X >= 0, z = X, X1 >= 0, X2 >= 0, X = X1, 1 + (1 + X) = X2
pi(z) -{ 3 }→ 2ndspos(X, 1 + X1 + X2) :|: X >= 0, z = X, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: X >= 0, z = X, Z >= 0, 1 + 0 = Z, X = 0
plus(z, z') -{ 1 }→ Y :|: z' = Y, Y >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(X, Y) :|: z = 1 + X, z' = Y, Y >= 0, X >= 0
square(z) -{ 1 }→ times(X, X) :|: X >= 0, z = X
times(z, z') -{ 2 }→ plus(Y, plus(Y, times(X', Y))) :|: z' = Y, Y >= 0, X' >= 0, z = 1 + (1 + X')
times(z, z') -{ 2 }→ plus(Y, 0) :|: z' = Y, Y >= 0, z = 1 + 0
times(z, z') -{ 1 }→ 0 :|: z' = Y, Y >= 0, z = 0
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ cons(X', 1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 3 }→ 2ndspos(z, 1 + X1 + X2) :|: z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(z - 1, z') :|: z' >= 0, z - 1 >= 0
square(z) -{ 1 }→ times(z, z) :|: z >= 0
times(z, z') -{ 2 }→ plus(z', plus(z', times(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
times(z, z') -{ 2 }→ plus(z', 0) :|: z' >= 0, z = 1 + 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
{ from } { 2ndsneg } { cons } { 2ndspos } { plus } { activate } { pi } { times } { square } |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ cons(X', 1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 3 }→ 2ndspos(z, 1 + X1 + X2) :|: z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(z - 1, z') :|: z' >= 0, z - 1 >= 0
square(z) -{ 1 }→ times(z, z) :|: z >= 0
times(z, z') -{ 2 }→ plus(z', plus(z', times(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
times(z, z') -{ 2 }→ plus(z', 0) :|: z' >= 0, z = 1 + 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ cons(X', 1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 3 }→ 2ndspos(z, 1 + X1 + X2) :|: z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(z - 1, z') :|: z' >= 0, z - 1 >= 0
square(z) -{ 1 }→ times(z, z) :|: z >= 0
times(z, z') -{ 2 }→ plus(z', plus(z', times(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
times(z, z') -{ 2 }→ plus(z', 0) :|: z' >= 0, z = 1 + 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: ?, size: O(n1) [3 + 2·z] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ cons(X', 1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 3 }→ 2ndspos(z, 1 + X1 + X2) :|: z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(z - 1, z') :|: z' >= 0, z - 1 >= 0
square(z) -{ 1 }→ times(z, z) :|: z >= 0
times(z, z') -{ 2 }→ plus(z', plus(z', times(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
times(z, z') -{ 2 }→ plus(z', 0) :|: z' >= 0, z = 1 + 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ cons(X', 1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 3 }→ 2ndspos(z, 1 + X1 + X2) :|: z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(z - 1, z') :|: z' >= 0, z - 1 >= 0
square(z) -{ 1 }→ times(z, z) :|: z >= 0
times(z, z') -{ 2 }→ plus(z', plus(z', times(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
times(z, z') -{ 2 }→ plus(z', 0) :|: z' >= 0, z = 1 + 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ cons(X', 1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 3 }→ 2ndspos(z, 1 + X1 + X2) :|: z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(z - 1, z') :|: z' >= 0, z - 1 >= 0
square(z) -{ 1 }→ times(z, z) :|: z >= 0
times(z, z') -{ 2 }→ plus(z', plus(z', times(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
times(z, z') -{ 2 }→ plus(z', 0) :|: z' >= 0, z = 1 + 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: ?, size: O(1) [0] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ cons(X', 1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 3 }→ 2ndspos(z, 1 + X1 + X2) :|: z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(z - 1, z') :|: z' >= 0, z - 1 >= 0
square(z) -{ 1 }→ times(z, z) :|: z >= 0
times(z, z') -{ 2 }→ plus(z', plus(z', times(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
times(z, z') -{ 2 }→ plus(z', 0) :|: z' >= 0, z = 1 + 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ cons(X', 1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 3 }→ 2ndspos(z, 1 + X1 + X2) :|: z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(z - 1, z') :|: z' >= 0, z - 1 >= 0
square(z) -{ 1 }→ times(z, z) :|: z >= 0
times(z, z') -{ 2 }→ plus(z', plus(z', times(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
times(z, z') -{ 2 }→ plus(z', 0) :|: z' >= 0, z = 1 + 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ cons(X', 1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 3 }→ 2ndspos(z, 1 + X1 + X2) :|: z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(z - 1, z') :|: z' >= 0, z - 1 >= 0
square(z) -{ 1 }→ times(z, z) :|: z >= 0
times(z, z') -{ 2 }→ plus(z', plus(z', times(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
times(z, z') -{ 2 }→ plus(z', 0) :|: z' >= 0, z = 1 + 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: ?, size: O(n1) [1 + z + z'] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ cons(X', 1 + (1 + X')) :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 3 }→ 2ndspos(z, 1 + X1 + X2) :|: z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(z - 1, z') :|: z' >= 0, z - 1 >= 0
square(z) -{ 1 }→ times(z, z) :|: z >= 0
times(z, z') -{ 2 }→ plus(z', plus(z', times(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
times(z, z') -{ 2 }→ plus(z', 0) :|: z' >= 0, z = 1 + 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 3 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 3 }→ 2ndspos(z, 1 + X1 + X2) :|: z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(z - 1, z') :|: z' >= 0, z - 1 >= 0
square(z) -{ 1 }→ times(z, z) :|: z >= 0
times(z, z') -{ 2 }→ plus(z', plus(z', times(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
times(z, z') -{ 2 }→ plus(z', 0) :|: z' >= 0, z = 1 + 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 3 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 3 }→ 2ndspos(z, 1 + X1 + X2) :|: z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(z - 1, z') :|: z' >= 0, z - 1 >= 0
square(z) -{ 1 }→ times(z, z) :|: z >= 0
times(z, z') -{ 2 }→ plus(z', plus(z', times(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
times(z, z') -{ 2 }→ plus(z', 0) :|: z' >= 0, z = 1 + 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: ?, size: O(1) [0] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 3 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 3 }→ 2ndspos(z, 1 + X1 + X2) :|: z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(z - 1, z') :|: z' >= 0, z - 1 >= 0
square(z) -{ 1 }→ times(z, z) :|: z >= 0
times(z, z') -{ 2 }→ plus(z', plus(z', times(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
times(z, z') -{ 2 }→ plus(z', 0) :|: z' >= 0, z = 1 + 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 3 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 4 }→ s' :|: s' >= 0, s' <= 0, z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(z - 1, z') :|: z' >= 0, z - 1 >= 0
square(z) -{ 1 }→ times(z, z) :|: z >= 0
times(z, z') -{ 2 }→ plus(z', plus(z', times(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
times(z, z') -{ 2 }→ plus(z', 0) :|: z' >= 0, z = 1 + 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 3 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 4 }→ s' :|: s' >= 0, s' <= 0, z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(z - 1, z') :|: z' >= 0, z - 1 >= 0
square(z) -{ 1 }→ times(z, z) :|: z >= 0
times(z, z') -{ 2 }→ plus(z', plus(z', times(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
times(z, z') -{ 2 }→ plus(z', 0) :|: z' >= 0, z = 1 + 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] plus: runtime: ?, size: O(n1) [z + z'] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 3 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 4 }→ s' :|: s' >= 0, s' <= 0, z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 }→ 1 + plus(z - 1, z') :|: z' >= 0, z - 1 >= 0
square(z) -{ 1 }→ times(z, z) :|: z >= 0
times(z, z') -{ 2 }→ plus(z', plus(z', times(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
times(z, z') -{ 2 }→ plus(z', 0) :|: z' >= 0, z = 1 + 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] plus: runtime: O(n1) [1 + z], size: O(n1) [z + z'] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 3 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 4 }→ s' :|: s' >= 0, s' <= 0, z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 + z }→ 1 + s'' :|: s'' >= 0, s'' <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
square(z) -{ 1 }→ times(z, z) :|: z >= 0
times(z, z') -{ 3 + z' }→ s1 :|: s1 >= 0, s1 <= 1 * z' + 1 * 0, z' >= 0, z = 1 + 0
times(z, z') -{ 2 }→ plus(z', plus(z', times(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] plus: runtime: O(n1) [1 + z], size: O(n1) [z + z'] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 3 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 4 }→ s' :|: s' >= 0, s' <= 0, z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 + z }→ 1 + s'' :|: s'' >= 0, s'' <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
square(z) -{ 1 }→ times(z, z) :|: z >= 0
times(z, z') -{ 3 + z' }→ s1 :|: s1 >= 0, s1 <= 1 * z' + 1 * 0, z' >= 0, z = 1 + 0
times(z, z') -{ 2 }→ plus(z', plus(z', times(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] plus: runtime: O(n1) [1 + z], size: O(n1) [z + z'] activate: runtime: ?, size: O(n1) [1 + 2·z] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 3 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 4 }→ s' :|: s' >= 0, s' <= 0, z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 + z }→ 1 + s'' :|: s'' >= 0, s'' <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
square(z) -{ 1 }→ times(z, z) :|: z >= 0
times(z, z') -{ 3 + z' }→ s1 :|: s1 >= 0, s1 <= 1 * z' + 1 * 0, z' >= 0, z = 1 + 0
times(z, z') -{ 2 }→ plus(z', plus(z', times(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] plus: runtime: O(n1) [1 + z], size: O(n1) [z + z'] activate: runtime: O(1) [8], size: O(n1) [1 + 2·z] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 3 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 4 }→ s' :|: s' >= 0, s' <= 0, z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 + z }→ 1 + s'' :|: s'' >= 0, s'' <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
square(z) -{ 1 }→ times(z, z) :|: z >= 0
times(z, z') -{ 3 + z' }→ s1 :|: s1 >= 0, s1 <= 1 * z' + 1 * 0, z' >= 0, z = 1 + 0
times(z, z') -{ 2 }→ plus(z', plus(z', times(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] plus: runtime: O(n1) [1 + z], size: O(n1) [z + z'] activate: runtime: O(1) [8], size: O(n1) [1 + 2·z] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 3 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 4 }→ s' :|: s' >= 0, s' <= 0, z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 + z }→ 1 + s'' :|: s'' >= 0, s'' <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
square(z) -{ 1 }→ times(z, z) :|: z >= 0
times(z, z') -{ 3 + z' }→ s1 :|: s1 >= 0, s1 <= 1 * z' + 1 * 0, z' >= 0, z = 1 + 0
times(z, z') -{ 2 }→ plus(z', plus(z', times(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] plus: runtime: O(n1) [1 + z], size: O(n1) [z + z'] activate: runtime: O(1) [8], size: O(n1) [1 + 2·z] pi: runtime: ?, size: O(1) [0] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 3 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 4 }→ s' :|: s' >= 0, s' <= 0, z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 + z }→ 1 + s'' :|: s'' >= 0, s'' <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
square(z) -{ 1 }→ times(z, z) :|: z >= 0
times(z, z') -{ 3 + z' }→ s1 :|: s1 >= 0, s1 <= 1 * z' + 1 * 0, z' >= 0, z = 1 + 0
times(z, z') -{ 2 }→ plus(z', plus(z', times(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] plus: runtime: O(n1) [1 + z], size: O(n1) [z + z'] activate: runtime: O(1) [8], size: O(n1) [1 + 2·z] pi: runtime: O(1) [4], size: O(1) [0] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 3 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 4 }→ s' :|: s' >= 0, s' <= 0, z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 + z }→ 1 + s'' :|: s'' >= 0, s'' <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
square(z) -{ 1 }→ times(z, z) :|: z >= 0
times(z, z') -{ 3 + z' }→ s1 :|: s1 >= 0, s1 <= 1 * z' + 1 * 0, z' >= 0, z = 1 + 0
times(z, z') -{ 2 }→ plus(z', plus(z', times(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] plus: runtime: O(n1) [1 + z], size: O(n1) [z + z'] activate: runtime: O(1) [8], size: O(n1) [1 + 2·z] pi: runtime: O(1) [4], size: O(1) [0] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 3 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 4 }→ s' :|: s' >= 0, s' <= 0, z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 + z }→ 1 + s'' :|: s'' >= 0, s'' <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
square(z) -{ 1 }→ times(z, z) :|: z >= 0
times(z, z') -{ 3 + z' }→ s1 :|: s1 >= 0, s1 <= 1 * z' + 1 * 0, z' >= 0, z = 1 + 0
times(z, z') -{ 2 }→ plus(z', plus(z', times(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] plus: runtime: O(n1) [1 + z], size: O(n1) [z + z'] activate: runtime: O(1) [8], size: O(n1) [1 + 2·z] pi: runtime: O(1) [4], size: O(1) [0] times: runtime: ?, size: O(n2) [2·z·z' + z'] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 3 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 4 }→ s' :|: s' >= 0, s' <= 0, z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 + z }→ 1 + s'' :|: s'' >= 0, s'' <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
square(z) -{ 1 }→ times(z, z) :|: z >= 0
times(z, z') -{ 3 + z' }→ s1 :|: s1 >= 0, s1 <= 1 * z' + 1 * 0, z' >= 0, z = 1 + 0
times(z, z') -{ 2 }→ plus(z', plus(z', times(z - 2, z'))) :|: z' >= 0, z - 2 >= 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] plus: runtime: O(n1) [1 + z], size: O(n1) [z + z'] activate: runtime: O(1) [8], size: O(n1) [1 + 2·z] pi: runtime: O(1) [4], size: O(1) [0] times: runtime: O(n2) [3 + 4·z + 2·z·z' + z'], size: O(n2) [2·z·z' + z'] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 3 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 4 }→ s' :|: s' >= 0, s' <= 0, z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 + z }→ 1 + s'' :|: s'' >= 0, s'' <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
square(z) -{ 4 + 5·z + 2·z2 }→ s5 :|: s5 >= 0, s5 <= 1 * z + 2 * (z * z), z >= 0
times(z, z') -{ 3 + z' }→ s1 :|: s1 >= 0, s1 <= 1 * z' + 1 * 0, z' >= 0, z = 1 + 0
times(z, z') -{ -1 + 4·z + 2·z·z' + -1·z' }→ s4 :|: s2 >= 0, s2 <= 1 * z' + 2 * (z' * (z - 2)), s3 >= 0, s3 <= 1 * z' + 1 * s2, s4 >= 0, s4 <= 1 * z' + 1 * s3, z' >= 0, z - 2 >= 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] plus: runtime: O(n1) [1 + z], size: O(n1) [z + z'] activate: runtime: O(1) [8], size: O(n1) [1 + 2·z] pi: runtime: O(1) [4], size: O(1) [0] times: runtime: O(n2) [3 + 4·z + 2·z·z' + z'], size: O(n2) [2·z·z' + z'] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 3 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 4 }→ s' :|: s' >= 0, s' <= 0, z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 + z }→ 1 + s'' :|: s'' >= 0, s'' <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
square(z) -{ 4 + 5·z + 2·z2 }→ s5 :|: s5 >= 0, s5 <= 1 * z + 2 * (z * z), z >= 0
times(z, z') -{ 3 + z' }→ s1 :|: s1 >= 0, s1 <= 1 * z' + 1 * 0, z' >= 0, z = 1 + 0
times(z, z') -{ -1 + 4·z + 2·z·z' + -1·z' }→ s4 :|: s2 >= 0, s2 <= 1 * z' + 2 * (z' * (z - 2)), s3 >= 0, s3 <= 1 * z' + 1 * s2, s4 >= 0, s4 <= 1 * z' + 1 * s3, z' >= 0, z - 2 >= 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] plus: runtime: O(n1) [1 + z], size: O(n1) [z + z'] activate: runtime: O(1) [8], size: O(n1) [1 + 2·z] pi: runtime: O(1) [4], size: O(1) [0] times: runtime: O(n2) [3 + 4·z + 2·z·z' + z'], size: O(n2) [2·z·z' + z'] square: runtime: ?, size: O(n2) [z + 2·z2] |
2ndsneg(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
2ndspos(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
activate(z) -{ 3 }→ s :|: s >= 0, s <= 1 * X' + 1 * (1 + (1 + X')) + 1, z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X1' + X2' :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2, X1' >= 0, X2' >= 0, X1 = X1', X2 = X2'
cons(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
from(z) -{ 1 }→ 1 + z :|: z >= 0
from(z) -{ 2 }→ 1 + z + X2 :|: z >= 0, X2 >= 0, 1 + (1 + z) = X2
pi(z) -{ 4 }→ s' :|: s' >= 0, s' <= 0, z >= 0, X1 >= 0, X2 >= 0, 0 = X1, 1 + (1 + 0) = X2
pi(z) -{ 3 }→ 0 :|: z >= 0, Z >= 0, 1 + 0 = Z, z = 0
plus(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus(z, z') -{ 1 + z }→ 1 + s'' :|: s'' >= 0, s'' <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
square(z) -{ 4 + 5·z + 2·z2 }→ s5 :|: s5 >= 0, s5 <= 1 * z + 2 * (z * z), z >= 0
times(z, z') -{ 3 + z' }→ s1 :|: s1 >= 0, s1 <= 1 * z' + 1 * 0, z' >= 0, z = 1 + 0
times(z, z') -{ -1 + 4·z + 2·z·z' + -1·z' }→ s4 :|: s2 >= 0, s2 <= 1 * z' + 2 * (z' * (z - 2)), s3 >= 0, s3 <= 1 * z' + 1 * s2, s4 >= 0, s4 <= 1 * z' + 1 * s3, z' >= 0, z - 2 >= 0
times(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
from: runtime: O(1) [2], size: O(n1) [3 + 2·z] 2ndsneg: runtime: O(1) [1], size: O(1) [0] cons: runtime: O(1) [1], size: O(n1) [1 + z + z'] 2ndspos: runtime: O(1) [1], size: O(1) [0] plus: runtime: O(n1) [1 + z], size: O(n1) [z + z'] activate: runtime: O(1) [8], size: O(n1) [1 + 2·z] pi: runtime: O(1) [4], size: O(1) [0] times: runtime: O(n2) [3 + 4·z + 2·z·z' + z'], size: O(n2) [2·z·z' + z'] square: runtime: O(n2) [4 + 5·z + 2·z2], size: O(n2) [z + 2·z2] |